Step of Proof: sq_stable__all
9,38
postcript
pdf
Inference at
*
1
I
of proof for Lemma
sq
stable
all
:
1.
A
: Type
2.
P
:
A
3.
x
:
A
. (
P
(
x
))
P
(
x
)
4.
(
x
:
A
.
P
(
x
))
5.
x
:
A
P
(
x
)
latex
by ((BackThruHyp 3)
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n
C
)) (first_tok :t) inil_term)))
latex
C
1
:
C1:
P
(
x
)
C
.
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
origin